COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Recent work in this Laboratory by R.S. Cartwright has led
C00008 00003	 December 1977: A report will be written outlining a more general
C00010 ENDMK
C⊗;
	Recent work in this Laboratory by R.S. Cartwright has led
McCarthy (1977) has discovered two new ways of characterizing
recursive programs in first order logic.  (Half of the first characterization
was discovered by R.S. Cartwright and is included in his Stanford PhD
thesis).  The idea leads to very direct informal proofs of correctness
in any first order system as well as formal proofs in a system like
FOL.  This work will be pursued both theoretically and experimentally
in the next eighteen months, but the results are so new that it is
difficult to be certain what milestones will be reached.  However, here
are some goals we are pretty certain we can reach:

1. Proof of correctness of a substantial  optimizing compiler like LCOM4.
March 1978.

2. Developing a practical system for proving correctness of Lisp
programs. - September 1978.

	Todd Wagner has developed a system for proving the correctness
of combinational and sequential digital circuits.  The system was
presented in at a March conference sponsored by  xx and was very
well received.  It has recently been discovered that the system
can be realized conveniently within FOL and Wagner will do it.
Estimated completion date - September 1977.
⊗ December 1977: A report will be written outlining a more general
theory of what a pattern is.  The theory encompasses temporal, spatial
and causal patterns as well as patterns of information in a data base.

⊗ December 1977: There are many more continuous functional than
those that have arisen in recursive definitions.  Recent work by
McCarthy in discovering new kinds will be followed up and a characterization
of the ones that arise in recursive definition will be made.  It looks
like the new kinds will be useful in expressing goals, and rules
for transforming them into the ordinary kind correspond to methods
for achieving goals.